COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.bb EXTENSIONAL FORMS
C00007 ENDMK
C⊗;
.bb EXTENSIONAL FORMS

	We will use ⊗extensional ⊗forms to form concepts
involving quantification, but the idea of extensional forms
doesn't depend on treating concepts as objects.
Indeed the main intended applications of extensional forms
are in mathematical theory of computation - the theory of the
correctness of computer programs.

	Consider first ordinary forms, i.e. expressions built
from symbols for constants, variables and functions and possibly
quantifiers and the Church lambda operator.  Such a form will
have certain free variables, and its value will depend on the
values assigned to the free variables.  We can call two forms
extensionally equivalent if they have the same value for all
assignments of values to the free variables they contain.  Thus
if + is given its usual interpretation on the integers, the
forms ⊗x+y and ⊗y+x are extensionally equivalent, but neither of
them is extensionally equivalent to ⊗u+v, because assigning ⊗x 
and ⊗y the value 0 and ⊗u and ⊗v the value 1 gives the forms
different values.

	Extensional forms can be regarded as the equivalence classes of this
equivalence relation, but instead of first introducing ordinary forms
and the equivalence relation, we will define extensional forms inductively
from the symbols for constants, variables, and functions.  In order to
motivate the reader's attention to a somewhat boring inductive
definition, we remark on the following virtues of extensional forms:
First they have no bound variables which simplifies the statement of
the laws of substitution, and second all the ways of building up
extensional forms are by the application of functions to constituent
forms; even ⊗λ(x,e) is just a function of two extensional forms ⊗x 
and ⊗e.  Consequently the syntax and semantics of extensional forms
can be axiomatized in first order logic.  This is important for the
applications to mathematical theory of computation and to the theory
of concepts.

	We start with a simplified theory:

Let ⊗D be a domain, e.g. the integers or people or concepts of integers
or concepts of people.  Let ⊗V be an infinite class of objects called
variables, and let ⊗E be another class of objects called environments.
Let %2value: V ~ E → D%1 be a distinguished function.  We will say call
%2value(x,e)%1 the value of the variable ⊗x in the environment ⊗e. 
We assume an axiom of extensionality for environments, namely

Ext!!ext1:	%2∀e1 e2.(∀x.(value(x,e1) = value(x,e2) ⊃ e1 = e2)%1.

Ext{eq ext1} implies that environments can be identified with certain
functions from variables to domain elements.  However, we cannot conclude
that all such functions are represented by environments.

	Next we have the assignment function %2assign: V~D~E → E.  It satisfies
the axioms

Ext!!ext2:	%2∀x d e.(value(x,assign(x,d,e)) = d)%1

and

Ext!!ext3:	%2∀x y d e.(y≠x ⊃ value(y,assign(x,d,e)) = value(y,e)%1.